\begin{tabbing}
$M$.sends($k$,$s$,$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$concat(map\=($\lambda$${\it pL}$.tagged{-}messages(2of(1of(${\it pL}$));$s$;$v$;2of(${\it pL}$))\+
\\[0ex];fpf{-}vals(product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);$\lambda$$p$.\=eqof(KindDeq)\+
\\[0ex](1of($p$)
\\[0ex],$k$);1of(\=2of(2of(2of(\+
\\[0ex]2of(2of(
\\[0ex]$M$)))))))))
\-\-\-
\end{tabbing}